../fix-syntax ../prism -javamaxmem 11g -cuddmaxmem 4g -heuristic speed -e 1e-6 -maxiters 1000000 zeroconf.prism zeroconf.props --property correct_min -const N=1000,K=8,reset=false
PRISM
=====
Version: 4.5.dev
Date: Fri Feb 26 16:24:02 CET 2021
Hostname: christopher
Memory limits: cudd=4g, java(heap)=11g
Command line: prism -javamaxmem 11g -cuddmaxmem 4g -heuristic speed -e 1e-6 -maxiters 1000000 zeroconf.prism zeroconf.props --property correct_min -const 'N=1000,K=8,reset=false'
Parsing model file "zeroconf.prism"...
Type: MDP
Modules: environment host0
Variables: b_ip7 b_ip6 b_ip5 b_ip4 b_ip3 b_ip2 b_ip1 b_ip0 n n0 n1 b z ip_mess x y coll probes mess defend ip l
Parsing properties file "zeroconf.props"...
2 properties:
(1) "correct_max": Pmax=? [ F (l=4&ip=1) ]
(2) "correct_min": Pmin=? [ F (l=4&ip=1) ]
---------------------------------------------------------------------
Model checking: "correct_min": Pmin=? [ F (l=4&ip=1) ]
Model constants: reset=false,N=1000,K=8
Warning: Switching to sparse engine and (backwards) Gauss Seidel (default for heuristic=speed).
Building model...
Model constants: reset=false,N=1000,K=8
Computing reachable states...
Reachability (BFS): 592 iterations in 52.90 seconds (average 0.089361, setup 0.00)
Time for model construction: 53.465 seconds.
Type: MDP
States: 1870338 (1 initial)
Transitions: 4245554
Choices: 3443961
Transition matrix: 154038 nodes (6 terminal), 4245554 minterms, vars: 58r/58c/7nd
Prob0E: 133 iterations in 3.78 seconds (average 0.028444, setup 0.00)
Prob1A: 91 iterations in 2.50 seconds (average 0.027451, setup 0.00)
yes = 17943, no = 611330, maybe = 1241065
Computing remaining probabilities...
Engine: Sparse
Building sparse matrix... [n=1870338, nc=2315321, nnz=2865855, k=4] [36.8 MB]
Creating vector for yes... [14.3 MB]
Allocating iteration vectors... [2 x 14.3 MB]
TOTAL: [79.6 MB]
Starting iterations...
Iteration 301: max relative diff=0.000018, 5.01 sec so far
Iterative method: 345 iterations in 7.59 seconds (average 0.016742, setup 1.82)
Value in the initial state: 5.04010521292984E-9
Time for model checking: 13.925 seconds.
Result: 5.04010521292984E-9 (value in the initial state)
Overall running time: 67.634 seconds.
---------------------------------------------------------------------
Note: There was 1 warning during computation.